COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Notes on chapter 3
C00004 ENDMK
C⊗;
Notes on chapter 3

The goal:
	After studying chapter 3 a student should have the following
competence.

	a. He can prove extensional properties of pure Lisp programs
including termination.

	b. He knows the limitations of the technique.

	c. Derived functions?

	d. Non-termination?

Problems of exposition:

	a. The basic idea is to use the Lisp definition of the function
as a first order functional equation.  However,
since Lisp functional programs are not to be presumed to be total,
we must use functions in places where we are inclined to think in
terms of predicates.  We will use bottom as a notation for undefined.
Therefore, the Lisp axioms need to be written
so as to cover the case in which some of the variables have value bottom.
It would be good to have a general definition principle for Lisp
functions that includes the case of non-totality.